COMMENT ⊗   VALID 00008 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\chapter{Proving facts about Lisp programs}
C00012 00003	\section{Introduction to Logic}
C00047 00004	\section{The basic S-expression domain }
C00073 00005	\section{Ordinals and Rank-induction}
C00094 00006	\section{Adding functions to {\bb S}}
C00109 00007	\section{The domains \qL!, \qAl!, \qN! and some functions on them}
C00117 00008	\section{summary of {\bb S}}
C00123 ENDMK
C⊗;
\chapter{Proving facts about Lisp programs}
\chaplab{provin}
	In this chapter and the next we begin the "Proving" part of the book.  
In particular we will explain a method for proving /extensional/
properties of a restricted but powerful class of LISP programs which we call
{\it clean, pure} \lisp\ programs.  This chapter is devoted to programs
known to terminate because of the structure of their recursions.  The
next chapter covers programs not known to terminate and includes techniques
for proving that they terminate for all arguments, terminate for some arguments
or don't terminate.

	We will give a number of simple examples 
to illustrate the method followed 
by a few more complex examples.
We will see in later chapters how the proof techniques can be extended to
cover a larger class of properties and a larger class of programs.

	While the ultimate aim of proving programs is to replace debugging
by computer checked proofs of program correctness, we aren't there yet.
However, even hand-checked proofs of correctness of small programs increase
our understanding of why programs work and improve the clarity and quality
of the programs we write.

	An {\it extensional property} is one that
depends only on the function computed by the program.
The fact that two sort programs compute the same function
and that /append/ is associative are extensional facts, but
that one sort program does $n↑2$ comparisons and another $n\ log\ n$
comparisons or that one program for /reverse/ does fewer /cons/es than
another are not.  These latter facts are examples of /intensional/ properties.
/Clean/ \lisp\ programs have no side effects (our
methods require the freedom to replace a subexpression by any
expression that can be proved to have the same value),
and equality refers to the S-expressions and not to
the list structures in memory that represent them.
/Pure/ \lisp\ involves only recursive function
definitions and doesn't use assignment statements.
So far we have only discussed how to write clean and pure \lisp
programs.   The constructs to be explained in Chapter[SECTION IMPURE]
will take us out of this realm.

	The basic idea is to represent both programs and the properties 
we want to prove about them as sentences in first order logic.  
The methods of first-order logic are well developed and understood.  
Although we present the proofs somewhat informally, they can easily
be fully formalized.  After a brief introduction to the idea of 
formalization, we give an informal exposition of first order 
logic and describe the theories of S-expressions, lists and natural numbers.  
Next come techniques for proving properties of programs known in advance 
to always terminate.  After this 
come the more difficult techniques required when termination cannot be
assumed and termination or non-termination must be proved.


	We attempt to motivate and intuitively justify the methods of
representation of programs, but no formal proof of soundness
is given.   Much of the material in
this chapter is based on [[Cartwright and McCarthy 1979]].
An extensive treatment of other program proving techniques
is given in [[Manna 1974]].

\noindent{\bf About Formalizing.}

	The main reason for developing formal methods is to be able to make
ideas and arguments clear and precise.  This is desirable for several reasons
For the logicians the development of formal systems and methods of reasoning
allowed them to eliminate paradoxes which arose in informal arguments and 
also to prove many interesting things about their systems.
For the computer scientist formalization provides a way of making notions 
and reasoning precise enough to be checked and even generated by a computer.  
One goal is to make the computer do as much of the work as 
possible.

	In a formal system there are notions of syntax (properties of
the expressions of the language as strings of symbols), semantics (rules
determining meanings of expressions, i.e. what things the expressions stand
for), and
rules for manipulating syntactic entities in a semantics preserving manner.
Thus there are expressions formed from some given collection of symbols in
a prescribed manner, a means of assigning meaning to these expressions,
and often a notion of deduction.

	For example, a programming system is a formal system.  It has a
language consisting of the programs, usually specified by some sort
of grammar and recognized by a parser.

	For reasoning about programs we will use a formal system based on
first order logic.  
Understanding properties of a system based on first  order logic can be 
often be reduced to understanding properties of the underlying logic.  
This underlying logic is powerful and in general well understood.   
Such systems are determined by three basic components:

1. a domain with some designated subdomains (called sorts),

2. a language whose function and predicate symbols are interpreted in the domain and 

3. a collection of facts that are true of the domain.  

	Given the basic  components, the expressions of the language, 
interpretation of these expressions
in the domain and rules for (syntactically) deducing additional facts
are fixed as we will explain below.

	Such a system can be mechanized in the following sense.  
We can write a program that is capable of understanding a description
of it, build a data structure representing the various components,
check that statements are well-formed expressions of the language,
and that an alleged proof is indeed a valid deduction from the known facts.
Given such a program, we can describe to it our system for proving facts about
LISP programs and it will be able to check that our proofs are correct.  
Such a program exists at Stanford [[Weyhrauch 1977]].
Other programs exist which are designed to automatically prove facts about 
LISP programs.  For example see [[Boyer and Moore 1978]].  

\section{Introduction to Logic}
\sectlab{logic}

	In this section we provide a succinct introduction to first order
logic, a tool that we shall use throughout this chapter to express properties of
programs and facts concerning our data domain . The reason for this formalism is
essentially twofold. Firstly it provides us with a convenient framework to work
within, a framework that allows for the possibility of computer checked proofs
and automated theorem proving . The second reason is that it enables us to
accurately specify the principles that we recognize as correct, and thus by
delineating them we specify what is to count as a proof and what is not.
\bigskip
\hbox to\hsize{\hss{\bf The Subject Matter}\hss}
 
 	Our aim is to describe the first order logic  of a particular
fixed structure ${\bb S}$. The one we have in mind is that of pure \lisp, which consists
of

   1. Domains: \qS!, \qL!, \qZ!, \qSy!$\ldots$

   2. Constants: |NIL|, |T|, 0, 1, 2, 3, $\ldots$

   3. Operations: \qa, \qd, \qcons, \qif, \qeq, \qat, +, -, $<, >, \ldots$

\noindent However in this section we shall work with an arbitrary structure ${\bb S}$ that consists
of

1. Domains: $A_1$, $A_2 \ldots  A_n$

2. Constants: $c_1, c_2, \ldots c_m$

3. Operations: $f_1, f_2, \ldots f_s$

4. Predicates: $P↓{A↓1}, P↓{A↓2},\ldots P↓{A↓n}$

\noindent Some remarks are in order. Firstly each $A_i$  is assumed to be a non-empty set of
objects. Secondly each operation $f_i$ is assumed to have an arity, namely the number of
arguments that it expects. In general it is also the case that the arguments must 
of a particular nature. For example the operation $f_i$ may be such that
$$f_i : A_{i_1} \times A_{i_2} \times \ldots \times A_{i_k} \longrightarrow A_{i_{k+1}}$$

\noindent which describes what sort of arguments $f_i$ requires and what sort of
values it returns. Let us leave aside the question of what happens when we feed
an operation of this sort 
the wrong sorts of arguments, we shall return to that later. In the meantime
the worried reader is advised to think of the operations as total, as indeed they will
,in the case of pure \lisp, turn out to be. The predicate $P↓{A↓i}$ is true of any
element $x$ of the domains    if and only if $x \in A_i$.
Finally each constant is assumed to belong to at least one of the sorts.

Our version of the first order logic that we use here is somewhat non-standard as
is our notion of 
a multi-sorted structure, our logic is different in that we allow lambda terms and our
notion of structure does not require that the domains be disjoint.
These differences are from a logical point of view inessential 
but from a practical point of view very important,
we shall not draw attention to them again.
\bigskip
\hbox to\hsize{\hss{\bf The Language}\hss}
 
	Corresponding to our structure ${\bb S}$ is its first order language, out of which 
we shall construct more complex syntactic
 expressions. These can be divided into two types,
logical and non-logical. The difference being that the later depends upon the nature
of ${\bb S}$ while the former does not. In our case they are

\noindent{\bf Logical: }

$$ \forall, \exists, \neg,\land, \lor, \supset, \lambda$$.

\noindent{\bf Non-logical: }

	     1. For each sort $A_i$ a countable set of variables $x_i, y_i, z_i,\ldots$

             2. A countable collection of general variables $x, y, z, \ldots $

	     3. For each constant $c_i$ a constant symbol $\hat c_i$.

	     4. For each operation $f_i$ an operation symbol $\hat f_i$.

	     5. For each predicate $P↓{A↓i}$ a predicate symbol $\hat {P↓{A↓i}}$.

	In usual treatments of first order logic one takes great pains to distinguish
between a constant or operation symbol and the corresponding constant or operation.
One of the advantages of working with a fixed domain is that the importance of
this distinction diminishes. Consequently from here on we shall not distinguish
between them, leaving context to do the work of $\hat{}$.

	Using this language we define the terms, function expressions,
predicate expressions and formulas
of the structure ${\bb S}$. The terms and function expressions are defined by mutual
recursion as follows.

\noindent{\bf Terms:}

1. Constant symbols and variables are terms.

       
2. If $\Psi$ is an n-ary function expression and $t_1, t_2 \ldots t_n$ are
terms then $\Psi [t_1,t_2, \dots t_n]$ is a term.

\noindent{\bf Function expressions:}

1. An m-ary operation symbol is an m-ary function expression.

2. If $\chi_1, \chi_2, \ldots \chi_m$ are general variables  and $t$ is a term
then
 $$[\lambda \chi_1, \ldots \chi_m .t]$$
 is an m-ary function expession.


	The idea here is that  variables of each sort are interpreted as 
ranging over their particular domain ($x_i$ over $A_i$) and the general
variables ranging over all the domains. Thus terms are  meant to be
interpreted as expressions that name elements of ${\bb S}$ and function
expressions name operations on the  domains. For example, in the case of
pure \lisp, some examples of terms are 

(i) |NIL|

(ii) $x$

(iii) $\qa x$

(iv) $\qif \qat x \qthen x \qelse \qd x$

\noindent Note that we will generally write 
$$\qif t↓0 \qthen t↓1 \qelse t↓2$$ 
instead of $\qif[t↓0,t↓1,t↓2]$. Some examples of function expressions are

(v) \qa

(vi) $[\lambda \chi . \qif \qat \chi \qthen \chi \qelse \qd \chi]$

	The predicate expressions and formulas in the first order language of ${\bb S}$ 
are also defined by mutual recursion.

\noindent {\bf Predicate expressions:}

1. The predicate symbols $A_iP$ are unary predicate expressions.

2. If $\chi_1 \ldots \chi_n$ are general variables and $\phi$ is a formula then
  $[\lambda \chi_1 \ldots \chi_n . \phi]$ is an n-ary predicate expression.

\noindent{\bf Formulas:}

1. If $t_1$ and $t_2$ are terms then $t_1 = t_2$ is a formula.

2. If $\Phi$ is an n-ary predicate expression and $t_1 \ldots t_n$ are terms
then $\Phi [ t_1 \ldots t_n]$ is a formula.

3. If $\phi_1$ and $\phi_2$ are formulas then so are $[\neg \phi_1], [\phi_1 \land 
\phi_2], [\phi_1 \lor \phi_2]$ and $[\phi_1 \to \phi_2]$.

4. If $\phi$ is a formula and $\chi$ is a variable then 
$\forall \chi \phi$  and
$\exists \chi \phi$ 
are formulas.

	Some examples of formulas, in the case of pure \lisp, are

(viii) $\qa x = \qd x$

(ix) $\qat x = |T|$

(x) $[[\neg \qat x] = |T|] \to \qa x = \qd x$

(xii) $\forall x [ [\neg \qat x = |T|] \to [\exists y \exists z [ x = y \qcons z]]]$

We say that a variable, $x$,is bound if it is in the lexical (textual) scope of a quantifier
of the form $\exists x$ or $\forall x$ or else occurs in the body $t$ of a lambda
expression of the form $\lambda y_1,\ldots x, \ldots y_k . t$ . To be perfectly
precise we should talk about bound occurrences of variables, we presume the reader is 
familiar with these concepts. An occurrence of a variable that is not bound is said
to be free .A sentence is a formula which contains no free occurences of variables.
\bigskip
\hbox to\hsize{\hss{\bf The Semantics}\hss}
 
	The semantics or meaning of these terms, function and predicate expressions 
and formulas
can now be explained. The first thing to observe is that although variables are
terms and terms are supposed to denote elements of our structure, there is very
little meaning one can give to a single solitary variable. It is for this reason
that most of the expressions listed above only have a interpretation with respect to a 
particular variable assignment. In our case we have sorted variables so well shall
spell out in detail what, in our situation, a variable assignment is.

 A {\bf variable assignment} $\nu $, is a function that assigns to each variable
(whether sorted or general) an element of one of the domains of ${\bb S}$ .
Furthermore it must do so in such a
fashion that if a variable is of a particular sort then its value under the
assignment must belong to the corresponding domain. In otherwords
$\nu(x_i) \in A_i$ for each variable $x_i$ of sort $A_i$. There are  no restrictions
on the particular domain that a general variables value must be in.

	Given a particular assignment $\nu$ we can give meanings to the terms, function
expressions and formulas that we have described. We do this by induction on the
way they are constructed. We begin with terms.

\noindent{\bf Terms:}
 The interpretation of a constant symbol is the constant that it denotes, while the
interpretation of a variable is the value that $\nu$ assigns to it.
If $\phi$ is a function expression taking $n$ arguments, and $t_1 \ldots t_n$
are terms, then the interpretation of $\phi[t_1 \ldots t_n]$ is the value 
of the function assigned to $\phi$ when applied to the values assigned to
the terms $t_1 \ldots t_n$.
Given a term $t$ we write $t↑\nu$ to denote the object it refers to under the 
assignment $\nu$.

For example in the case of pure \lisp\ , if the value assigned to $x$ is $|(A . B)|$
then the meanings of the terms given in examples (i)-(iv) above are:

(i)   |NIL|
  
(ii)   |(A . B)|
     
(iii)   |A|
      
(iv)   |B|
     

\noindent{\bf Function expressions:}
Operation symbols
are assigned the operations denoted by the symbol.
The expression  $[\lambda \chi_1, \ldots \chi_n .t]$ is assigned the function 
that is defined as follows.  The value
of $[\lambda \chi_1 \ldots \chi_n.t ][t_1 \ldots t_n ]$ is the value assigned to
$t$ relative to an interpretation which is modified by assigning the
values of the $t_i$s to the corresponding $\chi_i$s.
Given a function expression $\Psi$ we write $\Psi↑\nu$ to denote the function
it refers to under the particular assignment $\nu$.

The  reason for only allowing $\lambda$-binding
of general variables is that  if we allowed binding of sorted variables
then some applications would not result in well defined variable
assignments. In that a variable of a particular sort may be bound
to a value that did not lie in the appropriate domain.
   Another approach would be
to allow $\lambda$-binding of any variable, but only allow application of
such expressions to terms of the appropriate sort.  This makes
the class of well-formed expressions undecidable which is undesirable
if we wish to represent our system is in a computer. 

\noindent {\bf Predicate expressions:}
We have already specified the meanings of the predicates $P↓{A↓i}$, they simply
tell us whether or not an element belongs to the corresponding domain $A_i$.
The general situation is very similar to function expressions.
The predicate $[\lambda \chi_1 \ldots \chi_n . \phi]$ is true of the terms
$t_1 \ldots t_n$ under the assignment $\nu$ iff the formula $\phi$ is true
at the assignment that  differs from $\nu$ only in that it assigns the
value $t_i↑\nu$ to the variable $\chi_i$, for $i = 1 \ldots n$. If $\Phi$
is a predicate expression then we write $\Phi↑\nu$ for the resulting
predicate under the assinment $\nu$.

\noindent{\bf Formulas:}
The interpretation of a formula is the truth value assigned to it under the
variable assignment $\nu$. When a formula $\phi$ is true (in ${\bb S}$) under the 
assignment $\nu$ we write ${\bb S} \models \phi[\nu]$ . Thus by defining the 
relation $\models$ (called the satisfaction relation) we define the meanings of
the formulas. The definition is by induction on the construction of the formula
$\phi$.

1. If $\phi = [t_1 = t_2]$ then ${\bb S} \models \phi [\nu]$ iff $t↑\nu_1 = t↑\nu_2$

2. If $\phi = \Phi[t_1 \ldots t_n]$ then ${\bb S} \models \phi [\nu]$ iff
$\Phi↑\nu[t_1↑\nu \ldots t_n↑\nu]$.

3. If $\phi = [\neg \psi]$ then
${\bb S} \models \phi [\nu]$ iff
${\bb S} \not\models \psi [\nu]$
	
4. If $\phi = [\theta_1 \land \theta_2]$ then
${\bb S} \models \phi [\nu]$ iff
${\bb S} \models \theta_1[\nu]$ and
${\bb S} \models \theta_2[\nu]$.

5. If $\phi = [\theta_1 \lor \theta_2]$ then
${\bb S} \models \phi [\nu]$ iff
${\bb S} \models \theta_1[\nu]$  or
${\bb S} \models \theta_2[\nu]$.

6. If $\phi = [\theta_1 \to \theta_2]$ then
${\bb S} \models \phi [\nu]$ iff
${\bb S} \not\models \theta_1[\nu]$  or
${\bb S} \models \theta_2[\nu]$.

7. If $\phi = \forall \chi \psi$ then
${\bb S} \models \phi [\nu]$ iff
for every element $x$ in the domain that the variable $\chi$ ranges over
${\bb S} \models \psi [\nu↑x_\chi]$.
 Where $\nu↑x_\chi$ is the variable
assignment exactly like $\nu$ except that it assigns the value $x$ to
the variable $\chi$.

8. If $\phi = \exists \chi \psi$ then
${\bb S} \models \phi [\nu]$ iff
there is some element $x$ in the domain that the variable $\chi$ ranges over
such that ${\bb S} \models \psi [\nu↑x_\chi]$.

	Although this may look complicated, it is in fact quite straight
forward. An equality statement is true (w.r.t $\nu$) iff both sides of
the equality refer to the same object . The negation of a formula is true
iff the formula is false. A conjunction is true iff both conjuncts are
true and a disjunction is true iff one of the disjuncts is true. Finally
If $\chi$ is a variable, and $\phi$ is a formula, then
$\forall \chi \phi$ is true exactly if $\phi$ is true for all allowed
interpretations of the variables differing from the fixed one only in
assignment made to the variable $\chi$  .
$\exists \chi \phi$    is true exactly if there is some allowed
interpretation of the variable differing from the fixed one only in
assignment made to the variable $\chi$ .

	The reader should try as an exercise to see why the truth of a
sentence does not depend on the particular assignment. Thus it makes sense to
say that a sentence is true in a structure without ever mentioning variable 
assignments.

	Those who are familiar with the lambda calculus should note
that $\lambda$ is being used here in a very limited way.  Namely, the variables
in a lambda-expression take only elements of the domain as values,
whereas the essence of the lambda calculus is that they take arbitrary
functions as values.  We may call these restricted lambda expressions
{\it first-order lambdas}.
\bigskip
\hbox to\hsize{\hss{\bf Some laws of logic}\hss}
 

	As we said at the begining of this section one of the main reasons
for carrying out this formalism is that we can characterize what we regard
as a proof. The idea being that we shall start with certain given facts
about our structure ${\bb S}$. These being sentences in the first order
logic of ${\bb S}$. From these using certain rules of deduction we shall prove
other facts concerning ${\bb S}$. In our case the sentences that we will be most
interested in will express properties of operations or programs. We shall leave 
the discussion of non-logical axioms and the main proof principle until a later
section. What concerns us here is the very basic principles of deduction in
first order logic.
	We shall divide our discussion of the axioms into four parts, namely
boolean axioms, quantifier axioms, equality axioms and lambda axioms .These four
sets of axioms together with two  rules of inference constitute the logical
deduction system for our version of first order logic.

{\bf Boolean axioms:} We are quite generous in what we shall count as a
boolean or propositional axiom. But first we need to explain what a
tautology is.
 A propositional formula is a formula
that is built up from propositional constants $p, q, r, \ldots$
using the boolean connectives $\neg, \lor, \land$ and $\to$. A
propositional formula is said to be a {\it tautology}
if every assignment of truth values, \qtrue\ and \qfalse, to the propositional
atoms in it make the whole formula true. The simplest way to determine 
whether a propositional formula is a tautology is to use truth tables.
The meanings of the connectives being defined by the following table.


?????table????????


Now every formula $\phi$ in the language of ${\bb S}$ which can be obtained
from a propositional formula  $\psi$ by uniformly and simultaneously
substituting formulas of ${\bb S}$ for the propositional atoms in $\psi$
is a logical axiom of our system. This is a rather large collection
of axioms, nevertheless there is a mechanical procedure to decide
whether a formula of ${\bb S}$ belongs to this group of axioms. The main purpose
of these axioms is to free us from the rather trivial task of manipulating
the boolean operations of our logic.

{\bf Quantifier axioms:} The main reason that we introduced sorted variables
was to simplify the formulas that we will have to work with later. For 
example to express the fact that every element of domain $A_i$ has property
$\Phi$ we can write $\forall x_i \Phi(x_i)$ rather than $\forall x[ P↓{A↓i}[x]  \supset \Phi[x]]$
. However they make our axioms for introducing and eliminating quantifiers somewhat
more complex. Consequently we will first explain the axioms for quantifiers using
only the general variables, then explain the necessary modifications in the sorted
case. Also notice that $\exists x \phi$ has exactly the same meaning as the 
formula $\neg \forall x [ \neg \phi]$ which is why we will only state axioms
for the quantifier $\forall$ , treating the quantifier $\exists$ purely as an
abbreviation for the corresponding form involving $\forall$.

1. If $\phi$ and $\psi$ are formulas of ${\bb S}$ and $x$ is a general variable
not free in $\phi$, then the formula 
$$\forall x [ \phi \to \psi ] \to [ \phi \to \forall x \psi]$$
\noindent is an axiom.

2. If $\phi$ and $\psi$ are formulas and $\psi$ is obtained from $\phi$ by
substituing each free occurrence of the general variable $x$ in $\phi$ by the
term $t$, then as long as no variable free in $t$ becomes bound by this 
procedure
$$[\forall x \phi]  \to \psi$$
\noindent is an axiom.

The first set of axioms corresponds to universal introduction. The idea being
that if we derive $\psi$ from $\phi$ and $\phi$ contains no special
assumptions about the nature of $x$ then we can actually conclude $\forall x \psi$
from $\phi$ (Here we are also using one of our rules of inference that we will
describe later). This first sset of axioms does not need to be modified to
handle sorted variables, simply replace the word {\it general} by the word
{\it sorted} and the axioms remain valid.

The second set is rather more
troublesome. These axioms correspond to quantifier elimination
in that they allow us to conclude from $\forall x \Phi(x)$ that $\Phi(t)$ is true,
for any term $t$ (as long as the free variables that occur in $t$ do not
conflict with the bound variables in $\Phi$). The problem that arises with sorted
variables is that we should from $\forall x_i \Phi(x_i)$ only be able to conclude
that $\Phi(t)$ is true for those terms $t$  whose value lay in the particular
domain in question, in this case $A_i$.
For this reason we add the following axioms to the second set of axioms 

3. If $\phi$ and $\psi$ are formulas and $\psi$ is obtained from $\phi$ by
substituing each free occurrence of the sorted variable $x_i$ in $\phi$ by the
term $t$, then as long as no variable free in $t$ becomes bound by this 
procedure 
$$[[\forall x_i \phi] \land P↓{A↓i}[t]] \to \psi$$
\noindent is an axiom.

We remark that the  sentences $\forall x_i P↓{A↓i}[x_i]$ are also axioms, since they
simply express the conventions concerning our sorted variables.


{\bf Equality axioms:} These are very simple axioms that express the basic
properties of equality. Suppose $x$ and $y$ are any variables and that
$t$ is a term and $\phi$ is a formula, then the following are axioms.

1. $x = x$

2. $[x = y] \to [ t_v↑x = t_v↑y]$

3. $[x = y] \to [ \phi_v↑x \to \phi_v↑y]$

\noindent where  $t_v↑x$ and $\phi_v↑x$ denote the result of uniformly
substituting the variable $x$ for $v$.

{\bf Lambda axioms:} 
	The only rule required for handling lambda-expressions
in first order logic is called {\it lambda-conversion}.  It is essentially
one of

$[\lambda \chi .T   ][t] =$ the result   of substituting $t$ for $\chi$ in $T$.

\noindent or

$[\lambda \chi. \Phi][t] \Longleftrightarrow$ the result   of substituting $t$ for $\chi$ in $\Phi$.

\noindent depending on whether the lambda term is a predicate or function.

As examples of this rule, we have

$$[\lambda x .\qa x \qcons y][u \qcons v] = [\qa [u \qcons v]] \qcons y $$.

However, a complication requires modifying the rule.  Namely,
we can't substitute for a variable $x$ an expression $e$ that has a free variable
$x_1$ into a context in which $x_1$ is bound.  Thus it would be
wrong to substitute $x_1+x_2$ for $x$ in $\forall x_1  [x + x_1  = x_2]$ or into
the term $[\lambda x_1   x +  x_1][u + v]$.  Before doing the substitution, the
variable $x_1$ would have to be replaced in all its bound occurrences by
a new variable.  

	Lambda-expressions can always be eliminated from sentences and
terms by lambda-conversion, but the expression may increase greatly
in length if a lengthy term replaces a variable that occurs more than
once in $t$.  It is easy to make an expression of length proportional to $n$ whose
length is proportional to $2↑n$
after conversion of its $n$ nested lambda-expressions.
For example 
	
$$\lambda x_1.[x_1\qcons x_1][ ... [\lambda x_n .[x_n \qcons  x_n][A]] ... ]$$

becomes 

|(A . A)|

|((A . A) . (A . A))|

or

|((((A . A) . (A . A)) . ((A . A) . (A . A))) . ((A . A) . (A . A)) . ((A . A) . (A . A))))|
      
for $n = 1, 2,$ or $4$ respectively.

	The use of $\lambda$-expressions in writing programs also may improve
efficiency by specifying some the expression be evaluated once and
the value used in several places.  Where there are side-effects, of
course more than efficiency is affected.

	This completes our introduction to first order logic.
\section{The basic S-expression domain }
\sectlab{s-domain}

In this section we shall specify in detail our domain, {\bb S}, the so-called
s-expression domain. In practice however {\bb S} will be a dynamic object.
We shall often add new domains and more importantly new functions to it.
Our plan here is to introduce a simplified version of {\bb S} and
throughout this and subsequent sections add those entities that are
required for our treatment. This simplified version of {\bb S} consists
of the domains \qSy!, \qZ!, \qA!, \qC! and \qS!. These being symbols, integers,
atoms, cons cells (another name for non-atomic s-expressions), and finally
s-expressions. Let us be a little more specific concerning the nature
of these sets.

\qSy! : In pure \lisp\ the actual structure of symbols is irrelevant. All
that concerns us is that there are a lot of them, in fact a countably infinie
number of them. We shall continue to represent them as we did in chapter 1,
as strings of uppercase letters and symbols. There is one other important
fact about the set \qSy! namely that it contains the two elements 
\qT\ and \qNIL.

$$\qNIL,\ \qT \in \qSy!$$

\qZ! : The set of integers is a well known object and we waste no time
introducing it.

\qA! : The set of atoms is simply $\qSy! \cup \qZ!$. Consequently
$$[\qSy! \subset \qA!] \land [\qZ! \subset \qA!]$$

\qS! : As explained in chapter 1. the set of s-expressions is obtained from
the set of atoms by closing under a pairing operation. Again we shall not
be concerned with the actual nature of this operation, being content with
simply specifing certain properties it must possess. This we shall do in a
moment. The consequence of this definition of \qS! is that we have:
$$\qS! = \qA! \cup \qS! \times \qS!$$

\qC! : Is the set of non-atomic s-expressions, in some \lisp\ s they are called
pairs but we are adherring to the convention in \clisp. In other words
$\qC! = \qS! \times \qS!$.
 Notice that
$$[\qC! \cap \qA!=\emptyset]  \land [\qS! = \qA! \cup \qC!]$$

Before we proceed with the description of the functions and predicates of {\bb S},
we should mention another domain, namely \qL! the set of lists. We shall define
it and various subsets of it later. It is a part of our structure {\bb S} and we only
omit it here for simplicity.

The basic functions on \qS! are /car/, /cdr/ and /cons/, as the reader will be aware
they are represented by \qa, \qd\ and the infix \qcons\ in the external notation we
have been using. The reader should also be aware by now that /cons/ applied to
any to s-expressions is a non-atomic s-expression and that /car/ and /cdr/
applied to non-atomic s-expressions produce s-expressions. This can be 
expressed by the {\it domain mappings}:
$$\qa : \qC! \to \qS!$$
$$\qd : \qC! \to \qS!$$
$$\qcons\ : \qS! \times \qS! \to \qC!$$
Recall that in the previous section we suggested that the reader should
think of all the functions as being total. So if we are to be serious
about this we should explain what expressions like /car/[24] and /cdr/[0]
denote. For this and other reasons that we will not go into now (or later
for that matter) we extend our structure {\bb S} to include a new object
which all by itself makes up its very own domain. This new element is called
/bottom/ and is written:
$$\bot$$
and the domain that it belongs to is \qBot!. For the time being the reader
might like to think about $\bot$ as a /generic/ /error/ /message/ since it
will not be until we discuss programs that fail to terminate that its role
will be anything but this. It can also simply be viewed as an object which is
used to signify that a function is for some reason or other undefined.
 Another way of viewing bottom is that it is purely
a mathematical trick that enables one to represent partial functions as total
ones. We also state that $\bot$ is not an s-expression thus
$$\bot\not\in\qS!$$
 We can now make our functions /car/, /cdr/ and
/cons/ total by adopting the stance that
$$/car/[x] = \bot = /cdr/[x]$$
whenever $x \in \qA! \cup \qBot!$. Furthermore if either $x=\bot \lor y=\bot$ then
$$/cons/[x,y]=\bot$$
We shall make these conventions more explicit later. Now as we said last section
each domain has its own set of variables. This was done so that quantifying over a 
subdomain of \qS! would be particularly simple. In general we shall only do this when
it is convenient. For example having a set of variables that range over \qBot! will
not turn out to be very useful, so in this and other similar cases we relax this
conditon. In what follow we will abide by the following conventions.

$X,\ Y,\ Z, \ldots$ will be general variables, they are taken to range over
$\qS! \cup \qBot!$.

$x,\ y,\ z, \ldots$ will range over \qS!

$xx,\ yy,\ zz, \ldots$ will range over \qC!

$a,\ b,\ c,\ \ldots$ will range over \qA!

$n,\ m,\ i, j, \ldots$ will range over \qZ!

Another important fact about our domain {\bb S} is that it does not contain
any predicates. The job of the  $P↓\qC!$, $P↓\qA!$ and $P↓\qZ!$ for example
is done by the functions /consp/, \qat , /integerp/.
Where we have axioms of the form

{\bf Atom axiom:} $\forall a\ [\qat[a] = \qT] \land \forall xx [\qat[xx]=\qNIL]
\land \qat[\bot]=\bot$

We will not include for reasons that will become apparent a function
that corresponds to $P↓\qBot!$. All other domains will have a characteristic
function like the atom example above, that is explicitly in {\bb S} or
definable from functions already in {\bb S}. For example the domain
\qN! is easily recognizable using the functions /integerp/ and $>$ and the
constant $0$.

Using these conventions we can express the fundamental properties of
/car/, /cdr/ and /cons/. That were first mentioned in chapter 1.

{\bf Car axiom:} $\forall x,y\  \qa[ x\qcons y] = x \land \forall a \qa[a]=\bot = \qa[\bot]$

{\bf Cdr axiom:} $\forall x,y\  \qd[ x\qcons y] = x \land \forall a \qd[a]=\bot = \qd[\bot]$

since $x$ and $y$ are assumed to range over \qS!, the quantifier $\forall x,y$
can be read as {\it for all s-expressions x and y}. While the
quantifier $\forall a$ should be read as {\it for all atoms a}.
In \clisp\  $\qa \qNIL = \qd \qNIL = \qNIL$ , however the programs that appear
in this book will never rely on this oddity.
We also have:

{\bf Cons axiom:} $\forall xx \ \qa[xx]\qcons \qd[xx] = xx \land \forall X\ X\qcons\bot
=\bot\qcons X = \bot$

Since $xx$ is assumed to range over non-atomic s-expressions, the quantifier
$\forall xx$  expresses {\it for all non-atomic s-expressions} or
{\it for all cons cells} or even {\it for all pairs}.
The Cons axiom  also expresses the fact that two non-atomic s-expressions
are equal iff their a-parts and their d-parts are equal. In fact we can prove 
that the following is a fact about our structure {\bb S} soley on what we have 
developed up until now.


{\bf Eqpair Proposition:} 
$\forall xx,yy\ [[\qa xx = \qa yy] \land [\qd xx = \qd yy]] \liff [xx = yy]]$

{\bf Proof:} 
To prove that a formula of the form $A \iff B$ is true it is sufficient to
prove that $A \supset  B$ and $B \supset A$ are both true since equivalence is 
really  an abbreviation of the conjunction of the two implications.
So we must prove
$$[\qa xx = \qa yy] \land [\qd xx = \qd yy] \supset xx = yy$$
and
$$xx = yy \supset [\qa xx = \qa yy] \land [\qd xx = \qd yy]$$
To prove $A \supset B$ we assume $A$ and show that $B$ follows.
For the first implication, assume 
$$[\qa xx = \qa yy] \land [\qd xx = \qd yy]$$
Then by substitition of equals for equals we have
$$[\qa xx \qcons \qd xx] = [\qa yy \qcons \qd yy]$$
and using the cons axiom twice we obtain the desired conclusion
$$xx=yy.$$
For the second implication, assume 
$$xx=yy.$$ 
Then
$$[\qa xx = \qa yy] \land [\qd xx = \qd yy]$$
follows by subsititution.  This completes the proof.

$\qed↓{\bf eqpair}$

	The above proof was carried out in a 
"natural deduction" style and could be completely formalized
(for example so as to be accepted by a proof checker for
natural deduction style proofs)  without much additional detail.

[Remark:
A first order theory deduced by formal proof from given 
axioms will hold in any domain where the given axioms hold.  Thus
we are really proving things about a class of domains, not just
one.
]

Leaving aside the functions that operate on \qZ! we are left with the task
of describing the constants and the function \qeq\ as well as the 
\qif\ function which as we mentioned before we are writing it as
$$\qif \ldots \qthen \ldots \qelse \ldots$$
 The only properties of \qeq\ that are needed in the theory
of pure \lisp\  are the fact that $\qeq : \qS! \cup \qBot! \to \{\qT, \qNIL, \bot\}$
and the axiom

{\bf Eq axiom:} $$\forall a,b\ [[a \qeq b]=\qT \liff [a = b]]$$ 
and
$$\forall x,y\ [[x \qeq y]=\qT \supset [x=y]]$$
and
$$\forall X,Y\ [[X\qeq Y]=\bot] \supset [X = \bot  \lor  Y=\bot]$$

We should warn the reader that in most \lisp\ implementations large
integers may be equal but not \qeq.

In regard to the constants of our structure {\bb S} we make the 
stipulation that for every element of \qS! there is a constant that denotes
that object.
As in the external notation for \lisp programs, we will
use list and-or dot notation for S-expression constants. Thus
we have enough constants around to enable us never to worry about
constants again. There is however one important point to be made
here and that is that $\bot$ is an object in our structure {\bb S} but
it is not a part of pure \lisp\  in the sense that it should not
appear in the \lisp\ programs that the student writes.

{\bf Rules for Conditional Expressions.}

All the properties of the
$\qif \ldots \qthen \ldots \qelse \ldots$
construct follow from the following axiom

{\bf If Axiom:}
$$\forall x,X,Y\ [x \not= \qNIL] \supset
[[\qif x \qthen X \qelse Y]= X]$$
$$\forall X,Y\ [[\qif \qNIL \qthen X \qelse Y]= Y]$$
$$\forall X,Y\ [[\qif \bot  \qthen X \qelse Y]= \bot]$$



	It is worthwhile however to list separately some properties
of conditional terms.  First we have the obvious
$$[\qif \qtrue \qthen X \qelse Y] = X$$
$$[\qif \qfalse \qthen X \qelse Y] = Y$$

Next we have a /distributive/ /law/ for functions applied
to conditional terms, namely
$$f[\qif X \qthen Y \qelse Z] = 
[\qif X \qthen f[Y] \qelse f[Z]]$$
This applies to predicates as well as functions and can also be used
when one of the arguments of a function of several arguments is a
conditional term.  It also applies when one of the terms of
a conditional term is itself a conditional term.

	More facts about conditional terms are given in [McCarthy 1963]
including a discussion of canonical forms that parallels the canonical
forms of boolean terms.  Any question of equivalence of conditional
terms is decidable by truth tables analogously to the decidability of
propositional sentences.

We finish of this section with a discussion of the principle of
s-expression induction. It will turn out to be a special case of a
more powerful principle that we shall introduce in the next section.

{\bf The principle of S-expression induction.}

	With the axioms and domain facts given so far we can use
the rules of logic to prove many addiditonal facts about particular
S-expressions and a few general facts, but there are many facts
about S-expressions that can not be proved.  For example in the domain
of S-expressions we have

{\bf No-Rplacs:} $\forall x,y\ x\not=[x\qcons y]$

but this is not provable in the theory developed so far.  
Indeed there are domains where the facts given so far are true, 
but $\exists x,y\  x=[x\qcons  y]$ is also true.
(The significance of the title No-rplacs will become clear in
Chapter[IMPURE] where we discuss operations that create circular list
structures.)
This says that the algebraic and domain facts are insufficient
to characterize S-expressions.
Indeed G\"odel's famous theorem extends to tell us that no
theory in which all proofs can be checked admits proofs of all true
statements about S-expressions.  However, all practically interesting
sentences involving pure \lisp\ programs are provable in the above
theory supplemented by a suitable principle of mathematical induction.

	Recall the "inductive" definition of S-expression:
an S-expression is either an atom or 
it is the result of applying /cons/ to the  /car/ and the /cdr/.  
Furthermore each S-expression is the result of a finite number of
/cons/es begining with a finite number of atoms.  
Thus if some property is true of all atoms and 
whenever it is true of $x$ and $y$ it is true of $x\qcons y$ then 
it will be true of all S-expressions. We have already seen an application
and brief description of this principle in chapter 1.
It is expressed formally by the S-expression induction schema:

\noindent{\bf S-expression Induction:}
$\forall a \Phi[a] \land \forall xx  [\Phi[\qa xx]\land \Phi[\qd xx]\supset \Phi[xx]]
 \supset \forall x  \Phi[x]$.

Here $\Phi$ is a predicate parameter.  The schema is used by subsituting a unary
predicate expression (a formula with a designated variable which is to be
replaced by the argument to $\Phi$) for $\Phi$.  Thus the schema stands for
an infinite collection of axioms, one for each formula and designated
(free) variable that formula.
 Using S-expression induction we can prove 

{\bf No-Rplacs Proposition:} $\forall x,y\ x\not=[x\qcons y]$

{\bf Proof:}
Instantiating  the S-expression induction schema with $\Phi[x]$ being
$\forall y\ x\not= [x\qcons y]$  we obtain the
particular principle that if

$$\forall a,y\ a \not=[a\qcons y]$$
and
$$\forall xx\ [[\forall y\ \qa xx\not= [\qa xx\qcons  y]]
\land [\forall y\ \qd xx\not= [\qd xx\qcons y]] \supset 
\forall y\  xx\not=[xx\qcons y]]$$
then
$$\forall x,y\  x\not= x\qcons y$$ 

Thus to prove $\forall x,y\ x\not= x\qcons  y$   it is sufficient to prove the two clauses in
the hypothesis.  The clause for the ATOM case is 
$$\forall a,y\  a\not= a\qcons y$$
We prove it by contradiction.   That is we assume the negation, $a= a\qcons y $,
holds for some atom $a$ and S-expression $y$.  Then we have by the domain relations,
function mappings and the fact that $a$ ranges over atoms the following:

$$[a\in \qA! ] \land [a\qcons y \in \qC!] \land [\qA! \cap \qC! = \emptyset]$$

Putting this together we get $a \in \emptyset$, clearly a contradiction.

The clause for the non-ATOM case is

$$\forall xx  [\forall y  \qa xx\not=\qa xx\qcons y \land \forall y \qd xx\not=
\qd xx\qcons y  \supset \forall y  xx\not=  xx\qcons y]$$  

It is proved by assuming 
$$\forall xx\ [\forall y\ \qa xx\not= [\qa xx\qcons  y]]
\land [\forall y\ \qd xx\not= [\qd xx\qcons y]]$$
(the induction hypothesis) and deducing  $\forall y\ xx\not=  xx\qcons y]$
The latter is again done by contradiction.  Assume for some S-expression $y$
that $xx= xx\qcons  y$. 
Then by substitution and the  Car axiom we have $\qa xx=\qa [xx\qcons  y]=xx$.  
Substituting again we get $\qa xx=[\qa xx\qcons y]$ which contradicts the 
induction hypothesis, completing the proof.

$\qed↓{\bf no-rplacs}$

	S-expression induction is one example of a class of induction
principles known as "structural" induction.   Such principles are
based directly on the inductive definition of the domain to which
they apply.  Other examples are the principles of list and numerical
induction.
These are  structural induction principles and will also turn out to
be special cases of our general principle.
 Note that S-expression induction could be introduced as a proof rule
rather than an axiom schema.
To prove that some formula $\Phi[x]$ holds for all S-expressions, 
$x$  (i.e. to prove $\forall x \Phi[x]$)  it is sufficient to 

    (i) prove the ATOM case: $\forall  a  \Phi[ a]$ 

and

    (ii) assume the induction hypotheses: $\Phi[\qa xx]$ and $\Phi[\qd xx]$ and prove from them $\Phi[xx]$.

This is essentially what we did in carrying out the above proof.  
\section{Ordinals and Rank-induction}
\sectlab{rank}

In this section we introduce our main proof principle, that of rank induction.
A complete discussion of rank induction will require us to introduce
ordinals. For this reason we will begin by discussing a simplified version
of it. One where the rank of an s-expression is always a natural number. Let us 
state the principle first and then discuss its significance and truth.

Suppose $r$ is a function that assigns to each s-expression a natural number.
$$r\ :\ \qS! \to  \qN!$$
It is called a rank function because it can be thought of as assigning a /rank/
or measure of complexity to each s-expression. The principle of rank induction
in this case is the schema:

{\bf Rank Induction:}  $\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset
\Phi[x]] \supset \forall x \Phi[x]$

Here $\lambda z \Phi[z]$ is a predicate expression in the first order theory of
{\bb S} (we have written $\Phi[x]$ to abbreviate $[\lambda z \Phi[z]][x]$).
What the principle allows us to do is that if we find ourselves in a 
situation where the truth of $\Phi[x]$ follows from the assumption that $\Phi$
is true of all s-expressions of less rank than $x$. Then in fact we can conclude that
$\Phi$ is true of all s-expressions. The principle may seem a little 
mysterious at first, but hopefully the following informal proof of its truth
will make it seem a somewhat sounder principle.

{\bf Theorem:} The principle of rank induction is true, for all $\Phi$ and $r$ as
above.

{\bf Proof:} We shall argue by contradiction. Suppose that the principle
is false. In otherwords there is a predicate expression $\lambda z \Phi[z]$
such that
$$\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset \Phi[x]]$$
but that
$$\neg \forall x \Phi[x]$$
In otherwords  $$\exists x \neg\Phi[x]$$ by our quantifier axioms.
So let ${\cal X}$ be the set of all those s-expressions which do not have
the property $\Phi$
$${\cal X} = \{ x \in \qS! \mid \neg\Phi[x]\}$$
By our assumption ${\cal X}$ is non-empty. The key idea in the proof is 
to pick a  member of ${\cal X}$ that has a special property, namely that it
is of least rank. So let $y \in {\cal X}$ be such that
$$\forall x \in {\cal X}[ r(y) \leq r(x) ]$$
(another way of putting this is that $\forall x \in {\cal X}[r(y) \not> r(x)]$)
The reason why this is possible stems from a fundamental property of \qN!: All
non-empty subsets of \qN! have a least element. So in particular the set
$$\{n \in \qN! \mid \exists x \in {\cal X}[r(x) = n ]\}$$
has a least element $n↓0$ and by definition there must be a $y \in {\cal X}$
with $r(y)=n↓0$, this $y$ has the desired property.
Now because $y$ is a rank minimal element of ${\cal X}$ we have that
any s-expression of less rank cannot be in ${\cal X}$. This is just another way
of saying
$$\forall z [[r(z)<r(y)] \supset \Phi[z]]$$
now by our assumption and our quantifier axioms we have
$$[\forall z[[r(z)<r(y)]\supset \Phi[z]] \supset \Phi[y]]$$
Thus we conclude $\Phi[y]$ which unfortunately contradicts our choice of
$y$. So our initial assumption that the rank induction principle is false
was wrong and we are done.

$\qed↓{\bf rank\ induction}$


Observe that we really only used two facts about \qN!. Namely that it has an ordering
and that every non-empty subset has a least element. Sets with these two properties
are traditionally called well-ordered sets, and we shall discuss them in more detaii
in a moment. Before we do that however, we introduce an important rank function 
and using the corresponding version of rank induction we prove the principle of
s-expression induction.
$$r↓{sexp}(x)=\cases{0 & if $x \in \qA!$\cr
1+r↓{sexp}(\qa x) + r↓{sexp}(\qd x) &if $x \in \qC!$\cr}$$
This is an important function and we shall use it frequently. In fact we will
add it to our basic structure {\bb S} (the observant reader might have noticed
that up until now {\bb S} contained no rank functions, in the following section
we shall describe how we can extend {\bb S} by adding more rank functions. For
the time being $r↓{sexp}$ will suffice)

Notice that $r↓{sexp}$ has the following properties
$$r↓{sexp}(xx) > r↓{sexp}(\qa xx)$$
$$r↓{sexp}(xx) > r↓{sexp}(\qd xx)$$

{\bf Theorem:} The rank induction schema for $r↓{sexp}$ implies the principle of
s-expression induction.

{\bf Proof:} Assume the hypothesis of the principle of s-expression induction:
$$\forall a \Phi[a] \land \forall xx  [\Phi[\qa xx]\land \Phi[\qd xx]\supset \Phi[xx]]$$
Also let us assume the rank induction formula
$$\forall x[\forall y[[r↓{sexp}(y)<r↓{sexp}(x)]\supset \Phi[y]] \supset
\Phi[x]] \supset \forall x \Phi[x]$$
So all we need to prove is that 
$$\forall x[\forall y[[r↓{sexp}(y)<r↓{sexp}(x)]\supset \Phi[y]] \supset
\Phi[x]]$$
is true and we can conclude $\forall x\ \Phi[x]$.
In other words we have to prove that for every $x$ in \qS!
$$\forall y[[r↓{sexp}(y)<r↓{sexp}(x)]\supset \Phi[y]] \supset
\Phi[x]$$
is true. It is trivially true
if $x \in \qA!$ since we already have $\forall a\ \Phi[a]$.
So suppose that $xx$ is an arbitrary element of \qC! that satisfies
$$[\forall y[[r↓{sexp}(y)<r↓{sexp}(xx)]\supset \Phi[y]]$$
so because 
$[r↓{sexp}(xx) > r↓{sexp}(\qa xx)] \land [r↓{sexp}(xx) > r↓{sexp}(\qd xx)]$
we have
$$\Phi[\qa xx]\land \Phi[\qd xx]$$
and thus using the hypothesis of the s-expression principle we obtain
$$\Phi[xx]$$
In otherwords we have shown that
$$\forall x[\forall y[[r↓{sexp}(y)<r↓{sexp}(x)]\supset \Phi[y]] \supset
\Phi[x]]$$
and we are done
$\qed$

	In general restricting the rank induction principle to rank
functions with range in \qN! is not enough. In fact later on in this chapter
we will prove properties of a program which requires a rank function
whose domain is larger than just \qN!. As we saw above the principle of
rank induction is valid for any function $r$ whose range is a well ordered
set. For this reason we introduce ordinals, which are simply very nice well
ordered sets. Later on in sectref{list-alist} we shall show how ordinals
can be identified with a subset of \qL!. The ordinals are usually defined in
a very succinct fashion in a set theory. However since we do not presume
that the reader is familiar with any particular set theory we must be a 
little more sedate. We begin by giving some examples of ordinals.
 Any natural number is an ordinal, where we shall consider a natural
number to be identical to the set of numbers less than it. In otherwords
$$0 = \emptyset,\  1= \{0\},\ 2=\{0,1\},\ \ldots$$
 The first infinite ordinal is simply defined to be the set of all finite ordinals,
it is written $\omega$ and pronounced /omega/.  We then have the ordinals
$$\omega,\ \omega + 1,\ \omega+2,\ \omega +3,\ \ldots$$
where the operation of adding one to an ordinal $\kappa$ is defined as
$$\kappa + 1 = \kappa \cup \{\kappa\}$$
we can continue this process by defining
$$2\omega = \bigcup\{\omega+n\mid n \in \omega\}$$
Continuing  this process in the obvious fashion we obtain
$$\omega,\ \omega+1,\ \ldots\ 2\omega,\ 2\omega + 1,\ \ldots\ 3\omega,\ \ldots 4\omega,\ \ldots\ \omega.\omega $$
we usually write $\omega↑2$ for $\omega.\omega$.
There are three distinct types of ordinals $0$, successor ordinals (those that
are of the form $\kappa \cup \{ \kappa \}$ for some ordinal $\kappa$) and
limit ordinals like $\omega$ which are the union of all ordinals less than them
but are not successor ordinals. Continuing this process leads us to ordinals like
$$\omega↑2, \omega↑3, \ldots\, \omega↑\omega,\ldots\, \omega↑{\omega↑\omega},
\ldots\, \omega↑{\omega↑{\omega↑\omega}} \ldots\ $$
This process could be (and is by many set theorists) continued for a very very
long time. However we need only go a little further than we already have.
Let $\epsilon↓0$ be the union of the following sequence of ordinals
$$\omega, \omega↑\omega, \omega↑{\omega↑\omega},
\omega↑{\omega↑{\omega↑\omega}}
\omega↑{\omega↑{\omega↑{\omega↑\omega}}}
\omega↑{\omega↑{\omega↑{\omega↑{\omega↑\omega}}}}
\omega↑{\omega↑{\omega↑{\omega↑{\omega↑{\omega↑\omega}}}}}
\omega↑{\omega↑{\omega↑{\omega↑{\omega↑{\omega↑{\omega↑\omega}}}}}}
\omega↑{\omega↑{\omega↑{\omega↑{\omega↑{\omega↑{\omega↑{\omega↑\omega}}}}}}}
\ldots\ $$
It is the largest ordinal we shall ever use in this book. Its main claim to fame
other than that is that it is the smallest solution to the equation
$\omega↑x=x$ and appears in the following theorem of Cantors.

\noindent{\bf Cantors Normal Form Theorem:}
For any ordinal $\kappa < \epsilon↓0$ there exists a unique sequence of natural numbers
$$n↓0,n↓1, \ldots\ n↓m$$
and a unique sequence of ordinals less than $\kappa$
$$k↓0<k↓1< \ldots\ < k↓m$$
such that 
$$\kappa = n↓m.\omega↑{k↓m} + \ldots\ + n↓1.\omega↑{k↓1} + n↓0.\omega↑{k↓0}$$


We shall use this theorem to represent ordinals less than $\epsilon↓0$ as a
subset of \qL! in \sectref{list-alist}
The following is the traditional definition of an ordinal, it is somewhat abstract.

{\bf Definition of ordinals:} A set ${\cal X}$ is an ordinal if and only if
all its elements are themselves ordinals and  any element of ${\cal X}$ is
also a subset of ${\cal X}$.

The general principle of rank induction is simply:
If 
$$r\ :  \qS! \to \kappa$$
where $\kappa$ is an ordinal then

{\bf Rank Induction:}  $\forall x[\forall y[[r(y)<r(x)]\supset \Phi[y]] \supset
\Phi[x]] \supset \forall x \Phi[x]$

As an example to show the reader that ordinals are not terribly mysterious we
point out that the set of pairs of natural numbers ordered lexico-graphically,
i.e
$$n↓0\qcons n↓1 < m↓0\qcons m↓1 \liff \cases{ n↓0 < m↓0 &\cr n↓0=m↓0 \land n↓1 < m↓1 &\cr}$$
is a well ordered set that is isomorphic to $\omega↑2$. Similarly lists of $n$ 
integers ordered in an analagous fashion is a well ordered set isomorphic
to $\omega↑n$.

There is another form of induction which is equivalent to rank induction over
the ordinals that avoids the use of them. We finish of this section by
describing this form of induction.

{\bf Induction on Well-founded relation:}

	The general idea of induction on some domain involves a notion of 
	"smaller" on that domain which is /well-founded/.
  By well-founded we mean a well-ordered set with the modification that
the ordering need only be a partial ordering,(two elements need not be
comparable). An other way of phrasing the the fact that the set is 
well-founded that does not mention rank functions 
that every sequence of elements in which each element is smaller
(with respect to the partial ordering)
than the previous one must terminate after a finite number of steps.
Let $R$ be such a well-founded relation, we often write $<↓R$ to represent
the infix version of $R$.
Given a well-founded notion of smaller and a property $\Phi$, if it
is the case that whenever $\Phi$ holds for all elements smaller than
a given element then it also holds for that element, then we have $\Phi$
holds for all elements of the domain.  This can be formally expressed
by the schema

{\bf Induction over a well-founded relation:}
$\forall x[\forall y[[y<↓R x ]\supset \Phi[y]] \supset
\Phi[x]] \supset \forall x \Phi[x]$


	To see that this induction principle is "correct" suppose
the hypothesis holds and suppose there is some $x$ such that $\neg\Phi[x]$.
Then since $R$ is well-founded, there is a smallest $x$ such that $\neg\Phi[x]$
Otherwise we could find smaller counter examples ad-infinitum, forming
a nonterminating sequence of elements each of which is smaller 
(as measured by $R$) than its predecessor.  This contradicts the
well-foundedness of $R$.  If $x$ is the smallest counter example then
$$\forall x↓1\ [x↓1<x] ⊃ \Phi[x↓1]$$
therefore $\Phi[x]$ must hold
after all.  Hence there is no such counter example.

	As examples of well-founded relations on domains of immediate interest
we have 

\noindent $<$  the usual order relation on numbers

\noindent $<↓L$ on lists where $u <↓L v \liff u$ is a proper tail of $v$.  

\noindent$<↓S$ on S-expressions where $x <↓S y \liff 
x$ is a proper subexpression of $y$.  

Corresponding to these relations we have the following induction schemata:

\noindent \qN!-Induction\ :\  $\forall n  [\forall m  [m < n \supset \Phi[m]] ⊃ \Phi[n]]
\supset \forall n  \Phi[n]$

\noindent \qL!-Induction\ :\  $\forall u  [\forall v  [v <↓L u \supset \Phi[v]] ⊃ \Phi[u]]
\supset \forall u  \Phi[u]$ where $u,v$ range over lists.

\noindent \qS!-Induction\ :\  $\forall x  [\forall y  [y <↓S x \supset \Phi[y]] ⊃ \Phi[x]]
\supset \forall x  \Phi[x]$.

	Given domains $D↓1$ and $D↓2$ with well-founded orderings 
$<↓1,\ <↓2$ respectively there are a number of ways to construct new
orderings on combinations of these domains.  For example the
lexicographic ordering $<↓{12}$ on $D↓1\times D↓2$ is defined as the obvious
generalization of the integer example above.

Another means of defining a well-founded ordering is to induce one
by a mapping into a domain that has a well-founded ordering.
Thus if $r\ : D↓1 \to D↓2$ and  $<↓2$ is a well-founded ordering on $D↓2$
then the ordering $<↓r$ on $D↓1$ defined by 
$$ x <↓r y \liff   r(x)<↓2  r(y)$$
 is well-founded.
\section{Adding functions to {\bb S}}
\sectlab{adding funs}
          
The purpose of this section is to descibe how one can add functions
to the structure {\bb S}. This task in itself is not very interesting.
The real problem is to use the \lisp\  definition of the function
as the principle property of the new function. in such a way that
the added function behaves exactly as the \lisp\ program specifies.

In order to represent \lisp\ programs as functions in a first
order theory, we first need to represent the basic programs.  We have
already introduced /car/, /cdr/ and /cons/.  We have also added
the ternary function symbol \qif, to represent the conditional.

As in the external notation for programs.  We also add the function 
symbols \qequal, \qn, \qnot, \qand, \qor\  corresponding to external notation.
The axioms characterizing these functions are:

\noindent{\bf Equal axiom:}\ 

$\forall x,y  
[[x = y] \supset [x\qequal y]= \qT]\land 
[[x\not= y] \supset [x\qequal ]=\qNIL]$

and $\forall X [X \qequal \bot = \bot \qequal X = \bot]$

\noindent{\bf Null axiom:}\ $\forall x\ \qn x = [x \qeq \qNIL]$
and $\qn \bot = \bot$

\noindent{\bf Not axiom:}\ $\forall x\ \qnot x =[ \qif x \qthen \qNIL \qelse \qT]$
and $\qnot \bot = \bot$

\noindent{\bf And axiom:}\ $\forall x,y\ [x \qand y] =[ \qif x \qthen y \qelse qNIL]$

\noindent{\bf Or axiom:}\ $\forall x,y\ [x \qor y] =[ \qif x \qthen x \qelse y]$

For purposes of talking about \lisp\  programs we define the subclass
of terms in our language known as \lisp\  term.
Variables and S-expression constants are \lisp\  terms.  
If $f$ is one of the basic \lisp\  functions \qa, \qd, \qcons, 
\qequal, \qat, \qn, \qnot, \qand, or \qor, or the name of a function
representing a \lisp\  program, or a "new" function symbol and the arity
of $f$ is $n$, and $t↓0,\ t↓1,\ \ldots\ ,t↓n$ are \lisp\  terms then 
$f[t↓1,\ \ldots\  ,t↓n]$ and $[\lambda x↓1\ \ldots  x↓n\ .t↓0][t↓1,\ldots t↓n]$ are
\lisp\  terms.  And those are all the \lisp\  terms.  Notice that
these correspond to the terms of \lisp\  program definitions 
omitting the label construct and programs as arguments. Also notice that
$\bot$ is not a lisp term and so does not appear in programs.

The functions \qif,\ \qand,\ and \qor\ are exceptions to the rule that
we shall make explicit later. The gist of the rule is that our added
functions are call by value, this being expressed by the fact that
if any of the arguments to the function is $\bot$ then the value
of the function is also $\bot$. But let us do some more examples
before we face some of the subtlties, we begin with the program
/append/, we shall add to {\bb S} the function \qapp, the infix version
of /append/

	To do this we simply add the new function symbol \qapp\ to the language of {\bb S}
and add the defining equation.
$$\forall X,Y\ X\qapp Y = \qif \qn X \qthen Y \qelse \qa X \qcons [\qd X \qapp Y]$$
It is quite easy to see and not much harder to prove there is a unique function
from $\qS!\cup\qBot!$ to $\qS! \cup \qBot!$, that satisfies this equation.
We shall prove some interesting properties
of it in \sectref{simple}. However for the time being we are only concerned with
its proper definition. Notice that
$$\bot \qapp X = \bot = \qNIL\qapp \bot$$
follows from the defining equation and the if and null axioms. This is what we want
since all new defined functions are to be call by value. This will not always follow
from the program definition of the function. For example consider the rather useless
function
$$/always2/[x] \leftarrow 2$$
To add this function to our domain simply add the new function symbol /always2/
and the defining axiom
$$\forall x [ /always2/[x] = 2] \land /always2/[\bot] = \bot$$
Thus reflecting the fact that in most \lisp\  implementaions the arguments to
a function are evaluated before the body.


Let us now consider the general case so we can discuss some of the issues at hand.
Suppose we have a program for a function $f$
$$f[x] \leftarrow \tau[x,\ f]$$
where $\tau$ is a lisp term. Can we simply add to our domain {\bb S} a new function
$f$ which is defined by
$$\forall x\ f[x] = \tau[x,\ f] \land f[\bot]= \bot.$$
Well the answer to this question is almost. There are two problems that we must
overcome. The first is not very deep, $\tau[x,\ f]$ may have free variables other than
$x$ and  the function parameter $f$, consequently the function $f$ will depend
on the value of these free variables. In pure \lisp\  we have no way of assigning
values to free variables so we simply eliminate this possibility by stipulating
that $\tau$ does not have free variables other than $x$. The second problem is 
much more fundamental, the equation $f[x] = \tau[x,\ f]$ need not have a unique
solution. For an extreme example consider the program
$$/loop/[x] \leftarrow /loop/[x]$$
This program does not define any function and the corresponding equation is
satisfied by all functions.  If one actually typed the internal definition
of /loop/ to a \lisp\ the result would be a function that fails to terminate on any
input.
	In order to characterize recursive programs, we need some
way of expressing the fact that the function we mean is
the least defined solution of the functional equation.   We will do
this by introducing, in addition to the functional equation, a
schema called the /minimization/ /schema/ which expresses the fact that
every function satisfying the equation on the domain of definition is defined
at least every where that the function assigned to the program is defined,
and when both are defined, the have the same value. In otherwords the function
that we add is the least fixed point or solution to our defining equation.
So suppose that $\tau$ satisfies our condition concerning free variables
and we have defined the function
$$f[x] \leftarrow \tau[x,\ f]$$
and have the corresponding  axiom
$$\forall x\ f[x] = \tau[x,\ f] \land f[\bot]= \bot.$$
To this we add the new schema that expresses that $f$ is the smallest
solution. the socalled minimization schema.
$$\forall x [ \tau[x,g]\in \qS! \supset g[x]=\tau[x,g]] 
\supset \forall x [\tau[x,f]\in \qS! \supset f[x]=g[x]]$$

  Here $g$ is a function parameter.   This schema is really /schema/ /schema/, 
since for any particular term $\tau$ and function symbol $f$ we produce
from the schema a formula that still contains the parameter $g$  
We then must substitute some function expression of our language for $g$
to produce an axiom.  (This is similar to the induction schemas, except
there we substituted formulas for predicate parameters.) 

	The simplest application of the minimization schema is to show that 
the program for /loop/ given above computes the totally undefined function.
The minimization schema for loop is
$$\forall x [ g[x]\in \qS! \supset g[x]=g[x]] 
\supset \forall x [/loop/[x]\in \qS! \supset /loop/[x]=g[x]]$$

now let $g[x]$ be the totally undefined function, in otherwords let $g$ be the function
from  $\qS! \cup \qBot!$ to  \qBot! that has the property that
$\forall X\ g[X]=\bot$. Using this function in the minimization schema we can
conclude that
$$\forall x [/loop/[x]\in \qS! \supset /loop/[x]=g[x]]$$
because  
$$\forall x [ \bot\in \qS! \supset \bot=\bot] $$
is true since $\bot\not\in\qS!$. Thus we have
$$\forall x [/loop/[x]\in \qS! \supset /loop/[x]=\bot]$$
Now if we assume that $/loop/[x] \in \qS!$ for some $x$ we immediately obtain a 
contradiction since $x$ must be $\bot$ and $\bot\not\in\qS!$.

We can summarize the procedure for adding functions as follows.
Suppose that $\tau[x↓0,x↓1,\ldots\ x↓n, f]$ is a \lisp\ term whose free variables
are amongst $x↓0,x↓1,\ldots\ x↓n$ and $f$ is defined by the program
$$f[x↓0,x↓1,\ldots\,x↓n] \leftarrow \tau[x↓0,x↓1,\ldots\,x↓n,f]$$
then to add the so defined function to {\bb S} we merely add a new function symbol
$f$ to our language and the axioms, we let
$\bar x$ be $x↓0,x↓1, \ldots\, x↓n$
and $\bar X$ be $X↓0,X↓1, \ldots\, X↓n$

\noindent{\bf Program axiom:}\ 
$\forall \bar x\  f[\bar x] = \tau[\bar x,f]$

\noindent{\bf Bottom axiom:}\  
$\forall \bar X\ [ [X↓0=\bot \lor \ldots \lor X↓n=\bot]\supset f[\bar X] =\bot]$

\noindent{\bf Minimization scheme:}
$$\forall \bar x\  [ \tau[\bar x,g]\in \qS! \supset g[\bar x]=\tau[\bar x,g]] 
\supset \forall \bar x\ [\tau[\bar x,f]\in \qS! \supset f[\bar x]=g[\bar x]]$$

Under these conditions there is a unique function that has these properties.
Existance is not the most crucial property that we will be concerned with
(although it is obviously required for most other interresting properties).
We shall be interested in questions of /termination/ . For what values of its
arguments does the function have a value which is not $\bot$?
As an example of such a termination question we will show in \sectref{simple} that

\noindent{\bf Termination of \qapp\  :} if \qapp\ is defined as above then
$X*y \not= \bot \liff X\in \qL!$.

We shall also be very concerned with
more specific questions concerning the functions behaviour, in particular
formulating and proving properties that express the correctness of certain
programs.
\section{The domains \qL!, \qAl!, \qN! and some functions on them}
\sectlab{list-alist}

We now extend the basic structure {\bb S} in order to talk about the subdomain
of lists, alists and natural numbers.

\noindent{\bf Lists:}

\noindent Lists are defined by induction to be the smallest set
${\cal X}$ satsfying:

\noindent 1. $\qNIL \in {\cal X}$

\noindent 2. $u \in {\cal X} \supset [x\qcons u] \in {\cal X}$ for any $x \in \qS!$.

As mentioned previously we let \qL! denote the set of lists and 
we also let \qL{non-empty} denote all those lists
other than \qNIL. We let

$u,\ v,\ w,\ \ldots\ $ range over \qL!

$uu,\ vv,\ ww,\ \ldots\ $ range over \qL{non-empty}

\noindent Some obvious facts about these domains are
$$[\qL! \subset \qS!] \land [\qL{non-empty}\subset \qC!] \land 
[\qL{non-empty} \cup \{ \qNIL\}= \qL!] \land [\qL{non-empty} \cap \{\qNIL\} = \emptyset]$$
The behaviour of /car/, /cdr/ and /cons/ on this  domain is given by the 
mapping equations
$$\qa\ :\qL{non-empty} \to \qS!$$   
$$\qd\ :\qL{non-empty} \to \qS!$$   
$$\qcons\ : \qS! \times \qL! \to  \qL{non-empty}$$

	Since lists are a subdomain of S-expressions and non-empty lists
a subdomain of non-atomic S-expressions the axioms Car, Cdr and Cons 
apply to lists also.  For lists we have the following structural induction
principle which follows from the principle of rank induction either with
the rank function $r↓{sexp}$ or the rank function $r↓{list}$ defined by
$$r↓{list}(x) =\cases{ 0 & if $x \not\in \qL!$\cr
                       /length/[x] & otherwise\cr}$$


\noindent{\bf List  Induction:}
$\Phi[\qNIL] \land \forall uu  [\Phi[\qd uu]\supset \Phi[uu]] \supset \forall u  \Phi[u]$.

There are some important subsets of \qL! that we shall now define.

\noindent{\bf Alists:}

\noindent We have already introduce alists in  \sectref{numbers}. They are
formally defined to be the smallest set ${\cal X}$ satisfying

\noindent 1. $\qNIL \in {\cal X}$

\noindent 2. $u \in {\cal X} \supset [xx\qcons u] \in {\cal X}$ for any $xx \in \qC!$.

we denote the set of all alists by \qAl!.
By the definition a list is an alist if and only if all its members are non-atomic
s-expressions. We often use alists to represent finite functions, functions
whose domain is finite. The most important function of alists is /assoc/
that we defined in \sectref{numbers}. To accentuate the view of alists as finite
functions we sometimes write

$x \in dom(\alpha) \liff \neg\qn /assoc/[x, \alpha]$

If $x \in dom(\alpha)$ then $\alpha(x)=\qd /assoc/[x, \alpha]$

where we are letting

$\alpha, \beta, \delta, \gamma $ range over \qAl!
We let \qAl{non-empty} be  $\qL{non-empty} \cap \qAl!$.
\exercise Write a function /dom/ which given an alist returns its domain.
See the exercises on sets in \chapref{writin}.


\noindent{\bf Ordinals:} 

\noindent Using Cantors normal form theorem we can represent ordinals
less than $\epsilon↓0$ as special sorts of lists as follows. The idea is be to
define a function $\Omega$ from Ordinals to lists by recursion. The simplest case
being
$$\Omega( m.\omega↑n) = |((m . n))|$$
when $m$ and $n$ are natural numbers ($\omega↑0=1$).
and in general if $\kappa$ is a ordinal less than $\epsilon↓0$ and
$$\kappa = n↓m.\omega↑{k↓m} + \ldots\ + n↓1.\omega↑{k↓1} + n↓0.\omega↑{k↓0}$$
is its Cantor normal form then
$$\Omega(\kappa) = < [n↓m \qcons \Omega(k↓m)] \ldots\ [n↓1 \qcons \Omega(k↓1)]
 [n↓0 \qcons\Omega(k↓0)]>$$
Then we let $\qL{ordinal}= \{\Omega(\kappa)\mid \kappa < \epsilon↓0 \}$ .
So for example
$$\Omega(6)= |((6 . 0))|$$
$$\Omega(\omega↑{\omega↑{\omega↑\omega}})= |((1 . (1 . (1 . (1 . 1)))))|$$

{\bf Natural Numbers:}

Rather than axiomatize the integers we sketch the process for the subdomain
\qN!.
$$\qN! =\{ 0,1,2,3,4,5, \ldots\ \}$$
the main functions on \qN! are /1+/ and /1-/ the principle properties 
being essentially Peanos axioms.

\exercise Find out what Peanos axioms are and translate all of them except
the induction scheme into axioms about the functions /1+/ and /1-/.

If we add the following function to {\bb S} then the principle of rank induction
using this function implies the usual principle of mathematical induction on
the natural numbers.
$$r↓{num}[x] \leftarrow \qif P↓{\qN!}x \qthen x \qelse 0$$
The usual principle being

{\bf Induction on \qN!:}  $\forall n[\forall m[[m <  n ]\supset \Phi[m]] \supset
\Phi[n]] \supset \forall n \Phi[n]$

\section{summary of {\bb S}}
\sectlab{axiom-sum}
 
In this section we summarize the facts about the domain {\bb S}
mentioned so far.

{\bf Domains:}

\qS! , \qC! , \qBot! , \qA! , \qSy! , \qN! , \qZ! , \qL! , \qL{non-empty} , \qAl!
\qL{ordinal}.

{\bf Domain relations:}

$$\qSy! \subset \qA!$$
$$\qZ! \subset \qA!$$
$$\qN! \subset \qZ!$$
$$\qS! = \qA! \cup \qS! \times \qS!$$
$$\qC! = \qS! \times \qS!$$
$$\qC! \cap \qA!=\emptyset$$
$$\qS! = \qA! \cup \qC!$$
$$\qBot! \cap \qS!=\emptyset$$
$$\qL! \subset \qS!$$
$$\qL! = \{|NIL|\} \cup [ \qS! \times \qL!]$$
$$\qL{non-empty}\subset \qC!$$
$$\qL{non-empty} \cup \{ \qNIL\}= \qL!$$
$$\qL{non-empty} \cap \{\qNIL\} = \emptyset$$


{\bf Constants:}

$$\qNIL,\ \qT \in \qSy!$$
$$\bot\in\qBot!$$
$$0,1,\ldots\ \in \qN!$$


{\bf Variables:}

$X,\ Y,\ Z, \ldots$ will be general variables, they are taken to range over
$\qS! \cup \qBot!$.

$x,\ y,\ z, \ldots$ will range over \qS!

$xx,\ yy,\ zz, \ldots$ will range over \qC!

$u,\ v,\ w,\ \ldots\ $ range over \qL!

$uu,\ vv,\ ww,\ \ldots\ $ range over \qL{non-empty}

$\alpha, \beta, \delta, \gamma $ range over \qAl!

$a,\ b,\ c,\ \ldots$ will range over \qA!

$n,\ m,\ i, j, \ldots$ will range over \qZ!

We also remark that if $\chi$ ranges over a domain $D$ then we also use
$\chi↓0, \chi↓1, \ldots$ to range over $D$.

{\bf Functions and mapping equations:}

$$\qa : \qBot! \to \qBot!$$
$$\qa : \qA! \to \qBot!$$
$$\qa : \qC! \to \qS!$$
$$\qa : \qL{non-empty} \to \qS!$$
$$\qa : \qAl{non-empty}\to \qC!$$

$$\qd : \qBot! \to \qBot!$$
$$\qd : \qA! \to \qBot!$$
$$\qd : \qC! \to \qS!$$
$$\qd : \qL{non-empty} \to \qS!$$
$$\qd : \qAl! \to \qC!$$

$$\qcons\ : \qS! \times \qS! \to \qC!$$
$$\qcons\ : \qBot! \times \qS! \to \qBot!$$
$$\qcons\ : \qS! \times \qBot! \to \qBot!$$
$$\qcons\ : \qBot! \times \qBot! \to \qBot!$$
$$\qcons\ : \qS! \times \qL! \to \qL!$$
$$\qcons\ : \qC! \times \qL! \to \qAl!$$

$$/1+/ : \qZ! \to \qZ!$$
$$/1+/ : \qS!-\qZ! \to \qBot!$$
$$/1+/ : \qBot! \to \qBot!$$

$$/1-/ : \qZ! \to \qZ!$$
$$/1-/ : \qS!-\qZ! \to \qBot!$$
$$/1-/ : \qBot! \to \qBot!$$

{\bf Axioms:}

{\bf Car axiom:} $\forall x,y\  \qa[ x\qcons y] = x \land \forall a \qa[a]=\bot = \qa[\bot]$

{\bf Cdr axiom:} $\forall x,y\  \qd[ x\qcons y] = x \land \forall a \qd[a]=\bot = \qd[\bot]$

{\bf Cons axiom:} $\forall xx \ \qa[xx]\qcons \qd[xx] = xx \land \forall X\ X\qcons\bot
=\bot\qcons X = \bot$

{\bf If Axiom:}
$$\forall x,X,Y\ [x \not= \qNIL] \supset
[[\qif x \qthen X \qelse Y]= X]$$
$$\forall X,Y\ [[\qif \qNIL \qthen X \qelse Y]= Y]$$
$$\forall X,Y\ [[\qif \bot  \qthen X \qelse Y]= \bot]$$

{\bf Eq axiom:} $$\forall a,b\ [[a \qeq b]=\qT \liff [a = b]]$$ 
and
$$\forall x,y\ [[x \qeq y]=\qT \supset [x=y]]$$
and
$$\forall X,Y\ [[X\qeq Y]=\bot] \supset [X = \bot  \lor  Y=\bot]$$

\noindent{\bf Equal axiom:}\ 

$\forall x,y  
[[x = y] \supset [x\qequal y]= \qT]\land 
[[x\not= y] \supset [x\qequal ]=\qNIL]$

and $\forall X [X \qequal \bot = \bot \qequal X = \bot]$

{\bf Null axiom:}\ $\forall x\ \qn x = [x \qeq \qNIL]$
and $\qn \bot = \bot$

{\bf Not axiom:}\ $\forall x\ \qnot x =[ \qif x \qthen \qNIL \qelse \qT]$
and $\qnot \bot = \bot$

{\bf And axiom:}\ $\forall x,y\ [x \qand y] =[ \qif x \qthen y \qelse qNIL]$

{\bf Or axiom:}\ $\forall x,y\ [x \qor y] =[ \qif x \qthen x \qelse y]$